#ifndef BUFFER_OUTOFBOUNDS_HPP
#define	BUFFER_OUTOFBOUNDS_HPP


#include "cfg_visitor.hpp"
#include <set>
using namespace std;
class CFGvisitorFlatInfo;


class buffer_outofbounds {
public:
	buffer_outofbounds(const CFGvisitorFlatInfo& _flat, const IntervalAnalysis& _iv);
	set<label_t> out_of_bounds();
private:
	int array_size(array_element *ae);
	ASTnode* getPayload(label_t ell0) const;
	ASTnode* getPayload(CFGvertex *n) const;
	const CFGvisitorFlatInfo& flat;
	const IntervalAnalysis& iv;
};

#endif	/* BUFFER_OUTOFBOUNDS_HPP */

